%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Aufgabe
\Aufgabe[Bounded Model Checking\hfill\textbf{(1.5 Point)}]
Consider the following Program:

\lstinputlisting[basicstyle=\footnotesize]{main.c}

The Matrix $G$ models a graph with $N$ nodes, i.e, $G[i][j]$ is true iff there is a directed edge from node $i$ to node $j$. The method $\mathit{nondet}$ chooses an integer non-deterministically.

\begin{enumerate}
	\item Use CBMC to find the lowest value for $K$ such that the assertion at the end of the program can be violated. What does it mean that the error state is or is not reachable for a given graph $G$ and a given value $K$?
	\item Perform an unwinding of the loop for $K = 3$.
	\item Transform the unwinded program into the SSA form.
	\item Build an SMT formula from the SSA form which is satisfiable if and only if the assertion at the end of the program may be violated. {\em Note:} A call to $\mathit{nondet}$ can be modeled by introducing a new integer variable.
        \item Can you draw a conclusion about the satisfiability of the formula by comparing the value for $K$ that you determined under $(a)$ with the number of times the loop was unwinded for building the formula? Check whether the formula can be satisfied (You may use an SMT solver such as {\em Yices} or {\em Z3}) to be sure that the result of the satisfiability check is consistent with your expectation.
\end{enumerate}

\textbf{Solution} \\

a) We used webMC to verify that the lowest value for K to violate the assertion is $K = 4$. \\
This is rather easy to see since the given program produces an error if there is a circle of length K starting from node 0.\\
The only edge that leads back to node 0 is G[3][0]. Therefore, the loop must reach the value 3, which is only the case if $K \geq 4$.\\

b) Loop-unwinding for $K=3$: \\

\lstinputlisting[basicstyle=\footnotesize]{main_loop_unwinding.c}

c) Single static assignment form: \\

\lstinputlisting[basicstyle=\footnotesize]{main_ssa.c}

d) We built the following input for Microsoft's SMT-solver Z3, which can be found under the link: http://rise4fun.com/z3/ \\

{\tiny

\begin{verbatim}
; declare all variables that are of interest
(declare-const result1 Bool)
(declare-const result2 Bool)
(declare-const result3 Bool)
(declare-const result4 Bool)
(declare-const result5 Bool)

(declare-const node1 Int)
(declare-const node2 Int)
(declare-const node3 Int)
(declare-const node4 Int)

(declare-const next1 Int)
(declare-const next2 Int)
(declare-const next3 Int)

(declare-const nondet1 Int)
(declare-const nondet2 Int)
(declare-const nondet3 Int)

(declare-fun g(Int Int) Bool)

; defines the left-hand-side of the equation
(define-fun leftside() Bool
    (and (= result1 true) (= node1 0) 
         (= next1 nondet1) (= result2 (and result1 (g node1 next1))) (= node2 next1)
         (= next2 nondet2) (= result3 (and result2 (g node2 next2))) (= node3 next2)
         (= next3 nondet3) (= result4 (and result3 (g node3 next3))) (= node4 next3)
         (= result5 (and result4 (= node4 0) (> 3 0)))
    )
)

; a implies b is only false if a=true and b=false
(assert leftside)
(assert (implies leftside (not (not result5))))

; make sure that the nondet-values are in the range 0 <= nondet < 5
(assert (and (>= nondet1 0) (< nondet1 5 )))
(assert (and (>= nondet2 0) (< nondet2 5 )))
(assert (and (>= nondet3 0) (< nondet3 5 )))

; define the function g for inputs: row, column
(assert (and (= (g 0 0) false) (= (g 0 1) true)  (= (g 0 2) false) (= (g 0 3) false) (= (g 0 4) true )))
(assert (and (= (g 1 0) false) (= (g 1 1) false) (= (g 1 2) true)  (= (g 1 3) false) (= (g 1 4) false)))
(assert (and (= (g 2 0) false) (= (g 2 1) true)  (= (g 2 2) false) (= (g 2 3) true)  (= (g 2 4) false)))
(assert (and (= (g 3 0) true)  (= (g 3 1) false) (= (g 3 2) false) (= (g 3 3) false) (= (g 3 4) false)))
(assert (and (= (g 4 0) false) (= (g 4 1) false) (= (g 4 2) false) (= (g 4 3) false) (= (g 4 4) true )))

; check if the function is satisfiable and if so, obtain a model
(check-sat)
(get-model)
\end{verbatim}
}

The left hand side of the SMT-formula is defined in leftside(). It is a conjunction of all the assignments in program c). To make the function more readable, the range checks for the nondeterministic values have been put into additional assertions.\\
The right hand side is the negated assertion-condition: $\neg$ result5\\
The implication leftside $\Rightarrow$ result5 is therefore only satisfiable if the assertion is violated. (One could also apply the deduction theorem "backwards" and get rid of the implication.) \\

e) Since we found out in a) that $K \geq 4$ must hold in order to violate the assertion, the SMT formula must be unsatisfiable, since it was constructed with $K=3$. As expected, the formula is actually unsatisfiable. To see that the formula works as expected, one could change the return value of (g 2 0) to true. This would mean that there is a circle, e.g. "node0 to node1 to node2 to node0" of length 3 and Z3 would actually find this path.